…ernel

  Replace the closure-based NbE (Normalization by Evaluation) kernel with
  a direct environment-based approach where types are Exprs throughout.

  - Remove Value/Neutral/ValEnv/SusValue semantic domain (Datatypes.lean)
  - Replace Eval.lean with Whnf.lean (WHNF via structural + delta reduction)
  - Replace Equal.lean with DefEq.lean (staged definitional equality with
    lazy delta reduction guided by ReducibilityHints)
  - Rewrite Infer.lean to operate on Expr types instead of Values
  - Simplify TypecheckM: remove NbE-specific state (evalCacheRef, equalCacheRef),
    add whnf/defEq/infer caches as pure state
  - Add proof irrelevance, eta expansion, structure eta, nat/string literal
    expansion to isDefEq
  - Flatten app spines and binder chains in infer/isDefEq to avoid deep recursion

  Replace HashMap-based eqvCache with union-find EquivManager (ported from
  lean4lean) for congruence-aware structural equality caching. Add inferOnly
  mode that skips argument/let type-checking during inference, used for
  theorem value checking to handle sub-term type mismatches.

  Additional isDefEq improvements:
  - isDefEqUnitLike for non-recursive single-ctor zero-field types
  - isDefEqOffset for Nat.succ chain short-circuiting
  - tryUnfoldProjApp in lazy delta for projection-headed stuck terms
  - cheapProj=true in stage 1 defers full projection reduction to stage 2
  - Failure cache on same-head optimization in lazyDeltaReduction
  - Fix ReducibilityHints.lt' to handle all cases correctly

Move checkStrictPositivity/checkCtorPositivity into the mutual block as
monadic checkPositivity/checkCtorFields/checkNestedCtorFields, enabling
whnf calls during positivity analysis. This matches lean4lean's
checkPositivity and correctly handles nested inductives (e.g. an
inductive appearing as a param of a previously-defined inductive).

Split KernelTests.lean into Helpers, Unit, and Soundness submodules.
Add targeted soundness tests for nested positivity: positive nesting via
Wrap, double nesting, multi-field, multi-param, contravariant rejection,
index-position rejection, non-inductive head, and unsafe outer.

Add Lean.Elab.Term.Do.Code.action as an integration test case requiring
whnf-based nested positivity.

- Rewrite lam/forallE/letE inference to iterate binder chains instead of
  recursing, preventing stack overflow on deeply nested terms
- Add inductBlock/inductNames to RecursorVal to track the major inductive
  separately from rec.all, which can be empty in recursor-only Ixon blocks
- Build InductiveBlockIndex to extract the correct major inductive from
  Ixon recursor types at conversion time
- Fix validateRecursorRules to look up ctors from the major inductive
  directly instead of iterating rec.all
- Fix isDefEq call in lazyDeltaReduction (was calling isDefEqCore)
- Add regression tests for UInt64 isDefEq, recursor-only blocks, and
  deeply nested let chains

Switch all kernel caches from Std.HashMap to Std.TreeMap, replacing
hash-based lookups with structural comparison (Expr.compare, Level.compare).
Expr.compare is fully iterative using an explicit worklist stack, and
Expr.beq/liftLooseBVars/instantiate/substLevels/hasLooseBVarsAbove now
loop over binder chains to avoid stack overflow on deeply nested terms.
Add pointer equality fast paths (ptrEq) for Level and Expr, and a
pointer-address comparator (ptrCompare) for the def-eq failure cache.

  - Track letValues/numLetBindings in TypecheckCtx so whnfCore can
    zeta-reduce let-bound bvars by looking up stored values
  - Thread let context through iterativized binder chains in infer
    (lam, forallE, letE) and isDefEqCore (lam/pi flattening, eta)
  - Add isProp that checks type_of(type_of(t)) == Sort 0 and rewrite
    isDefEqProofIrrel to use it with withInferOnly
  - Fix K-reduction to apply extra args after major premise
  - Add cheapBetaReduce for let body result types
  - Whnf nat primitive args when they aren't already literals
  - Skip whnf/whnfCore caches when let bindings are in scope
  - Increase maxRecursionDepth to 10000

…f into mutual block

  Move whnf/whnfCore/unfoldDefinition from Whnf.lean into the Infer.lean
  mutual block so they can call infer/isDefEq (needed for toCtorWhenK,
  isProp in struct-eta, and checkRecursorRuleType). Add new Primitive.lean
  module that validates Bool/Nat inductives and primitive definitions
  (add/sub/mul/pow/beq/ble/shiftLeft/shiftRight/land/lor/xor/pred/charMk/
  stringOfList) against their expected types and reduction rules. Validate
  Eq and Quot type signatures at quotient init time.

  Key changes:
  - checkRecursorRuleType: builds expected type from recursor + ctor types,
    handles nested inductives (cnp > np) with level/bvar substitution
  - checkElimLevel: validates large elimination for Prop inductives
  - toCtorWhenK: infers major's type and constructs nullary ctor (was stub)
  - tryEtaStruct: now symmetric (tries both directions) with type check
  - isDefEq: add Bool.true proof-by-reflection, fix bvar quick check to
    return none (not false) on mismatch, add eta-struct fallback for apps
  - Safety/universe validation in infer .const, withSafety in checkConst
  - Constructor param domain matching and return type validation
  - Hardcode ~30 new primitive addresses in buildPrimitives
  - Add unit tests for toCtorIfLit/strLitToConstructor/isPrimOp/foldLiterals
  - Add soundness tests for mutual recursors, parametric/nested recursors
  - Previously failing RCasesPatt.rec_1 now passes

Kernel2 implements normalization-by-evaluation with Krivine machine
semantics and call-by-need thunks for O(1) beta reduction, replacing
the substitution-based approach. Includes both Lean (Ix/Kernel2/) and
Rust (src/ix/kernel2/) implementations with FFI bridge, plus extensive
test suites (unit, integration, Nat, Rust FFI).

Kernel1 improvements:
- Canonical level normalization based on Géran's algorithm
- Context-aware whnf caching with ptr-equality binding context checks
- Native reduction support (reduceBool/reduceNat) for native_decide
- Nat reduction handles both .lit and Nat.zero constructor forms

Lean + Rust kernel: extend nat primitive reduction beyond concrete values
to handle symbolic step cases (add/sub/mul/pow/beq/ble with succ/zero
args), add O(1) nat literal ↔ ctor/neutral def-eq without allocating
constructor chains, and add isDefEqOffset for Nat.succ chain
short-circuiting. New helpers: extractSuccPred/PredRef, isNatZeroVal
in both Lean and Rust.

Performance: add inference cache (ptr_id-keyed), whnf_core cache, thunk
pointer short-circuit in spine comparison, pointer-based failure cache
for same-head delta, eager beta in eval (skip thunk allocation for
lambda heads), bidirectional check (push Pi codomain through lambda
bodies), and apply_pmm_and_extra to consolidate recursor application.

Correctness: validate K-reduction major premise type against inductive
(to_ctor_when_k_val), enforce unsafe/partial safety on constants, flatten
nested projection chains, WHNF struct before projection in eval, detect
@[eagerReduce], apply whnf_core after delta steps in lazy delta loop,
handle nat lit iota reduction directly (Lit(0)/Lit(n+1) → rule without
ctor conversion), and preserve binder names through quoting.

…me components

  Remove Lit(NatVal(n+1)) matching from extractSuccPred (Lean + Rust) to
  prevent O(n) recursive peeling in symbolic step-case reductions — literals
  are already handled in O(1) by computeNatPrim. This eliminates the PredRef
  enum (Rust) and Sum return type (Lean), simplifying all call sites.

  Fix parse_name in FFI to handle French-quoted numeric components
  («0» → Name.num) instead of treating all dotted segments as strings.

  - Add closure environment equivalence short-circuit in isDefEq for lam/pi,
    skipping eval when bodies match and envs are equiv-manager equivalent
  - Extend EquivManager with reverse map (node→ptr), findRootPtr, and
    non-allocating tryIsEquiv for second-chance cache lookups
  - Add ptr success cache alongside failure cache in isDefEq
  - Use equiv-root-aware lookups in whnf and whnf_core caches
  - Register structural sub-component equivalences after successful isDefEq
  - Switch Rust closure environments from Vec<Val> to Rc<Vec<Val>> (COW)
  - Fix lazy delta hint ordering to match Lean's lt'-based priority (not height)
  - Add second whnf_core pass (cheapProj=false) before full whnf in isDefEq
  - Block delta-unfolding of fully-applied nat primitives stuck on symbolic args
  - Add natPred reduction and shiftLeft/shiftRight symbolic step-cases
  - Fix iota reduction to only match nat literals for the real Nat type
  - Use per-constant expr cache in Rust convert (fixes cross-constant level bugs)
  - Make Expr/Level BEq ignore non-semantic metadata (names, binder info)
  - Treat theorems as Regular(0) not Opaque for delta unfolding
  - Use bidirectional check (not infer+isDefEq) for theorem values
  - Fix List universe level in string literal primitives
  - Improve Rust error messages and Display impls for KExpr/Val/Name
  - Add diagnostic counters and trace instrumentation throughout

- Fix proof irrelevance to check proof *types* are Prop (not the proofs themselves)
- Fix iota reduction field indexing to use nfields instead of numParams
- Fix projection whnf to preserve pointer identity when inner struct is unchanged
- Allow K-reduction to fall through to standard iota on failure
- Add System.Platform.numBits reduction (WordSize) for platform-dependent constants
- Add keep_alive vec to prevent Rc address reuse corrupting equiv_manager
- Fix lazy_delta quick check to exclude same-head-const (matching Lean4 semantics)
- Use full is_def_eq (not structural-only) in step 10 of def-eq algorithm
- Recurse whnf_core after iota/quotient reduction results
- Fix reduceNative to handle universe level instantiation and canonicalize results
- Extract Stats into dedicated struct in both Lean and Rust with detailed counters
- Add typecheckConstWithStatsAlways to capture stats even on heartbeat errors
- Add 700+ lines of Rust unit tests and 240+ lines of Lean unit tests for parity
- Skip universe/safety validation in infer_only mode
- Add bidirectional check fast path via structural Expr comparison before isDefEq